A:Realizer, i:Id. R-has-loc(A;i)  R-ds(A;i) =   x:Id fp Type 

latex

Definitions

x:A. B(x), P  Q, b, R-has-loc(R;i), R-ds(R;i), Prop, t  T, x. t(x), false, if b t else f fi, P  Q, P  Q, P  Q, P & Q, true, A, {T}, Realizer, Unit, x(s), False, , , , left  right, @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, @loc effect knd(v:T)  x := f State(ds) v , sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc precondition for a(v:T):P State(ds) v, @loc: k writes only members of L, @loc: k sends only on links in L, @loc: only members of L read x

Lemmas

unit wf, Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, fpf-empty wf, not wf, false wf, all functionality wrt iff, assert wf, bor wf, R-has-loc wf, fpf-join wf, R-ds wf, id-deq wf, implies functionality wrt iff, not functionality wrt iff, assert of bor, eq id wf, ifthenelse wf, fpf-single wf, assert-eq-id, bool wf, iff transitivity, eqtt to assert, bnot wf, eqff to assert, assert of bnot, lsrc wf, es realizer wf, assert-fpf-is-empty, fpf-join-is-empty, fpf-trivial-subtype-top, top wf, assert of band, fpf-is-empty wf